La version 4.05.0 du langage OCaml vient d’être publiée, le 13 juillet 2017 ; quelque mois après la sortie de la version 4.04.0, annoncée le 4 novembre 2016. OCaml est un langage fonctionnel de la famille des langages ML (dont font partie SML et F#). Il s’agit d’un langage fonctionnel multi‐paradigme fortement typé qui permet de mélanger librement les paradigmes fonctionnel, impératif et objet.
Il s’agit des deux premières versions après le passage à un cycle court de développement (6 mois). Elles contiennent assez peu de changements majeurs et peuvent être considérées comme des versions de maturation, en particulier pour la nouvelle phase d’optimisation Flambda introduite dans la version 4.03.
On note cependant l’intégration de deux nouveaux outils dans le compilateur : un profileur de mémoire et un fuzzer ; mais aussi quelques améliorations du langage et de la bibliothèque standard. Pas mal de changements ont aussi eu lieu dans les entrailles du compilateur et n’ont pas encore débouché sur des changements visibles à la surface du langage.
Une des nouveautés les plus surprenantes de ces cycles de développement est probablement l’apparition d’une nouvelle syntaxe alternative à OCaml, nommé Reason(ml), sous l’impulsion d’une équipe de Facebook.
Sommaire
Outils de développement
Du côté des outils de développement, deux nouveaux outils ont été intégrés à la distribution OCaml: un profileur de mémoire, Spacetime, et un fuzzer, afl-fuzzer.
Spacetime: profileur de mémoire
Le nouveau profileur de mémoire baptisé spacetime n’est pas activé par défaut à cause de son impact sur la performance et la mémoire des processus profilés. Il est cependant aisément disponible à travers un switch opam, le gestionnaire de paquets d’OCaml qui gère aussi les versions installées du compilateur Ocaml. Installer un compilateur OCaml avec le prise en charge de spacetime activée se fait avec une simple ligne :
$ opam switch 4.05.0+spacetime
Une fois spacetime activé, n’importe quel programme peut être profilé en définissant la variable d’environnement OCAML_SPACETIME_INTERVAL
. On peut, par exemple, s’intéresser à la consommation mémoire lors de l’analyse des dépendances du compilateur :
$ OCAML_SPACETIME_INTERVAL=50 codept ocaml-compiler
Les traces sont ensuite sauvegardées sous la forme spacetime-$process-id
et peuvent être analysées grâce à l’outil perf_spacetime
qui dispose d’un mode terminal et d’un mode service Web permettant d’explorer en détails la consommation mémoire.
Dans le cas illustré, on peut voir que la consommation de la mémoire se structure en cycles composés d’une phase d’exploration durant laquelle la consommation de la mémoire croît, suivie d’une phase de résolution qui permet au ramasse‐miettes de collecter la majorité de la mémoire utilisée dans la phase précédente.
Intégration de afl-fuzzer
American fuzzy lop (aussi connu sous le nom de afl-fuzzer) est un fuzzer, c’est‐à‐dire un outil pour tester des logiciels en leur injectant des données aléatoires en entrée.
Contrairement à la plupart des fuzzers, afl-fuzzers va plus loin que la simple injection de données aléatoires non corrélées : il observe le comportement interne du programme testé pour essayer de forger des données d’entrée qui vont explorer de nouvelles branches du code à éprouver. Cela permet d’améliorer le taux de couverture du test, au prix d’une nécessaire instrumentation du code. La mouture 4.05 d’OCaml permet désormais d’ajouter cette instrumentation au code compilé grâce à une simple option de compilation.
Comme exemple basique d’utilisation, on peut considérer ce code qui échoue sur un cas très particulier :
let () =
let s = read_line () in
if String.length s > 5 then
match s.[0], s.[1], s.[2], s.[3], s.[4] with
| 'e', 'c' , 'h', 'e', 'c' -> failwith "Échec improbable"
| _ -> ()
Pour analyser ce code avec afl fuzzer, il suffit d’utiliser la nouvelle option -afl-instrument
d’ocamlopt, fournir quelques cas de base, puis de lancer afl-fuzz lui‐même, qui va utiliser un algorithme générique sur ces cas de base pour générer de nouveaux cas à tester :
ocamlopt -afl-instrument test.ml
afl-fuzz -i input -o output ./test.ml
Ce dernier trouve rapidement que, par exemple, echec#Ε$5<ȹpu|Ϧģ
fait planter le programme. Cependant, il n’est pas assuré de trouver une entrée minimale (ici « echec ») faisant échouer le programme.
Évolution du langage OCaml
Exceptions locales
Parmi les particularités d’OCaml, il y a ces exceptions qui sont suffisamment rapides pour être utilisées en tant que structures de contrôle. OCaml 4.04 introduit une notation simplifiée pour les exceptions locales :
let recherche_premier (type a) predicat table=
let exception Trouve of a in
try
Array.iter (fun x -> if predicat x then raise (Trouve x) ) table;
None
with
Trouve x -> Some x
Avant l’introduction de cette nouvelle notation, il fallait passer par un module local pour définir l’exception :
let recherche_premier (type a) predicat table=
let module M = struct exception Trouve of a end in
try
Array.iter (fun x -> if predicat x then raise (M.Trouve x) ) table;
None
with
M.Trouve x -> Some x
De plus, dans le futur, ces exceptions locales pourraient faire l’objet d’optimisations spécifiques.
Ouverture locale de module dans les motifs
Une des nouveautés d’OCaml 4.04 est la possibilité d’ouvrir localement un module à l’intérieur d’un motif :
module M = struct
type t = A | B | C
type u = List of t list | Array of t array
end
let est_ce_la_liste_ABC x = match x with
| M.( List [A;B;C] ) -> true
| _ -> false
Comme dans le cas des expressions, ouvrir localement un module permet d’importer les types et valeurs dans la portée (scope) courante sans polluer la portée en dehors du motif. Cette construction permet également de rétablir une certaine symétrie entre motifs et expressions, comme dans l’exemple suivant uniquement valide depuis OCaml 4.04 :
module N = struct
type r = { x : int }
end
let N.{ x } (* { x } est un motif ici *) =
N.{ x = 1 } (* { x = 1} est une expression de ce côté-ci *)
Représentation en mémoire optimisée
Il est désormais possible d’optimiser la représentation en mémoire des variants avec un seul constructeur et un seul argument ou des enregistrements avec un seul champ en les annotant avec [@@unboxed]
:
type 'a s = A of 'a [@@unboxed]
type 'a r = { f: 'a } [@@unboxed]
Sans l’annotation [@@unboxed]
, ces deux types seraient représentés en mémoire sous la forme d’un bloc OCaml composé d’un en‐tête et d’un champ :
┌────────┬───────────┐
│ entête │ champs[0] │
└────────┴───────────┘
Pour des types plus complexes, l’en‐tête contient des informations sur le nombre de champs dans le bloc et sur l’étiquette du constructeur. Cependant, pour ces cas particuliers, l’en‐tête n’apporte aucune information et il est possible de l’élider.
Cette optimisation est particulièrement utile dans le cadre des types algébriques généralisés, puisqu’elle permet d’introduire des types existentiels sans payer de coût en mémoire. Par exemple, si l’on souhaite oublier le type des éléments d’une liste, on peut introduire le type algébrique généralisé suivant :
type liste = Any: 'a list -> liste [@@unboxed]
Grâce à l’annotation [@@unboxed]
, le type liste
aura exactement la même représentation en mémoire qu’une liste classique, et représente une version du type 'a list
qui interdit toute manipulation dépendante du type 'a
des éléments de la liste.
Dans la plupart des cas, cette optimisation est transparente à l’usage. Cependant, les bibliothèques de liaison (bindings) C‐OCaml doivent faire attention à ce changement de représentation en mémoire. Afin d’éviter de briser les bibliothèques de liaison existantes, cette optimisation n’est pas activée par défault, mais doit l’être au cas par cas avec l’annotation[@@unboxed]
ou via l’option de compilation -unboxed-types
.
Vers des chaînes de caractères immuables
La migration vers des chaînes de caractères immuables, initiée dans OCaml 4.02, se poursuit avec l’apparition d’une option de configuration du compilateur permettant d’en faire le comportement par défaut. Cette option n’est pas encore activée par défaut dans 4.05, mais des discussions sont en cours pour l’activer dans la prochaine version (4.06).
Évolution de la bibliothèque standard
La bibliothèque standard continue d’évoluer doucement, soit pour pallier des incohérences, avec par exemple l’introduction d’une fonction map
pour les ensembles Set
, soit pour s’adapter à l’évolution du code idiomatique OCaml, avec par exemple l’ajout de variantes de fonctions utilisant des options plutôt que des exceptions pour gérer les éléments manquants dans des Set
ou des Map
.
Amélioration du compilateur
Ces deux cycles de développements auront vu aussi un grand nombre d’améliorations internes du compilateur et de son écosystème : le système de construction du compilateur est en train de subir un sévère ménage de printemps, tandis que les tests d’intégration continue ont été améliorés, notamment pour mieux supporter les anciennes versions de Windows. Parallèlement, un travail de fond est en cours pour améliorer le déverminage de programme OCaml et préparer le changement de modèle de mémoire nécessaire pour une future version multicœur d’OCaml.
Ces évolutions n’apportent pas encore de changements visibles pour la plupart des utilisateurs, mais devraient porter leurs fruits dans les versions à venir.
Un changement plus visible, même s’il ne concerne essentiellement que des utilisateurs experts, est l’intégration progressive d’une architecture de greffons (plugins) dans le compilateur. Pour l’instant, ces greffons peuvent, par exemple, transformer l’arbre de syntaxe abstrait comme le ferait un préprocesseur basé sur les points d’extensions, effectuer une passe de vérification supplémentaire sur les types inférés par le vérificateur de type du compilateur, ou encore modifier la représentation interne Lambda.
Reason
En dehors de l’évolution du langage lui‐même, un projet inhabituel est né récemment dans les locaux de Facebook1. Ce projet se nomme Reason et a pour but de rénover la syntaxe d’OCaml. Il a été initié par un petit groupe mené par Jordan Walke (le créateur initial de la bibliothèque React).
L’objectif
La raison de Reason (huhu !) est que la syntaxe d’OCaml rebute certaines personnes. Cependant, OCaml s’inscrit de plus en plus dans le milieu industriel (comme le montrent les exemples de Facebook, mais aussi Jane Street, dans une tout autre mesure). Dans un désir de démocratisation, l’équipe ReasonML décida de créer une nouvelle syntaxe pour OCaml du nom de Reason. Comparé à la syntaxe originale d’OCaml, Reason se rapproche de la syntaxe de JavaScript. Par exemple, les accolades et les points‐virgules font un retour en force :
let hello name_opt =
let name = match name_opt with
| None -> "world"
| Some x -> x in
Format.printf "Hello %s!" name
devient :
let hello name_opt => {
let name = switch name_opt {
| None => "world";
| Some n => n;
};
Format.printf "Hello %s!" name
}
D’une certaine manière Rust
a eu la même idée en proposant une syntaxe très proche du C++
. Elixir rejoint le même objectif dans une autre mesure.
La syntaxe de Reason essaye également d’augmenter la cohérence interne de la syntaxe et de corriger des erreurs historiques. Par exemple, les constructeurs de types se lisent de droite à gauche comme les fonctions dans Reason :
type constructeur_de_type 'argument = { id:int, x:'argument }
L’objectif est, bien entendu, plus large et a amorcé notamment un élan autour des outils qui peuvent aider le développeur à utiliser OCaml. Le top‐level interactif amélioré utop
, qui semble unanimement reconnu comme étant l’outil pour tester du code OCaml, fut réutilisé pour Reason et l’accueil auprès des nouveaux développeurs (extérieurs à la communauté OCaml) fut couronné de succès.
Le service d’aide à l’édition merlin
, qui permet d’intégrer la coloration syntaxique, mais aussi l’inférence de type dans les éditeurs, eut aussi son intégration avec Reason et tout ceci apporta une légitimité à la continuation de ces projets pour Reason mais aussi pour OCaml.
Enfin, le gestionnaire de paquets opam
reste toujours la pierre angulaire de l’écosystème d’OCaml et donc l’est aussi par définition pour Reason. Ce dernier se voit donc désormais utilisé par des gens n’ayant pas forcément en tête les subtilités de l’écosystème d’OCaml (comme ocamlfind
).
Au‐delà de cette nouvelle syntaxe, l’équipe de Reason attache donc une attention particulière à l’environnement de développement d’OCaml. Cela permet notamment d’apporter une réelle critique extérieure aux outils de développement OCaml et en particulier une critique justifiée sur la difficulté de prise en main de ces outils pour un débutant.
Ce qu’est Reason
Reason n’est ni plus ni moins qu’une option dans le compilateur. Nous parlons ici de l’option -pp
qui permet de remplacer la partie frontale du compilateur par un préprocesseur ad hoc. Le préprocesseur Reason prend donc du code Reason en entrée, le transforme en arbre de syntaxe abstrait OCaml et passe cet arbre au compilateur OCaml classique.
Ceci permet entre autres de garder la compatibilité avec l’existant et de profiter à la fois des logiciels et bibliothèques déjà développés en OCaml et de la nouvelle syntaxe Reason, et réciproquement. Il existe d’ailleurs un outil permettant de convertir du code OCaml vers du code Reason !
Partager la partie centrale du compilateur permet également d’utiliser les différents back‐ends disponibles pour OCaml. En particulier, OCaml dispose de deux back‐ends JavaScript : js_of_ocaml et bucklescript. Le premier, js_of_ocaml, est plus ancré dans l’écosystème OCaml, tandis que le second, bucklescript, est plus tourné vers l’écosystème JavaScript et dispose d’une intégration avec npm, un gestionnaire de paquets JavaScript.
Grâce à ces back‐ends, l’équipe ReasonML a pu convertir environ 25 % du code de FaceBook Messenger en code Reason.
Un avenir imprévisible
On peut cependant s’interroger sur l’interaction de la communauté OCaml existante et de cette nouvelle communauté Reason, bien plus centrée sur le Web, l’écosphère JavaScript et npm. Les atomes crochus n’abondent pas forcément entre ces deux communautés.
Le bon point reste tout de même l’ouverture de l’écosystème d’OCaml à des développeurs qui ne faisaient pas de l’OCaml. Cela permet notamment d’apporter des perspectives neuves et de revitaliser des problématiques de développement parfois oubliées dans l’écosystème OCaml.
Le succès n’est peut‐être pas au rendez‐vous et le projet a encore besoin de faire ses preuves auprès d’un large public (problématique qu’on peut corréler avec Hack auprès de ceux qui font du PHP d’ailleurs). Mais le retour ne semble être que bénéfique au final pour l’ensemble des communautés !
-
elle a été extérieure puisqu’elle a été initiée par Facebook alors que ce dernier ne faisait pas encore partie du consortium OCaml. ↩
Aller plus loin
- Site officiel (397 clics)
- Discours officiel (49 clics)
- Manuel OCaml : spacetime, profileur de mémoire (37 clics)
- Manuel OCaml : afl-fuzz (37 clics)
- Manual OCaml : exceptions locales (24 clics)
- Reason (127 clics)
- Annonce officielle de la 4.05 (27 clics)
- Annonce officielle de la 4.04 (19 clics)
- Dépêche LinuxFr.org sur OCaml 4.03 (40 clics)
# Coquille ?
Posté par GuieA_7 (site web personnel) . Évalué à 2.
Dans le dernier exemple :
est-ce que ça ne serait pas 'switch name_opt' plutôt ? (désolé si je dis des bêtises je ne parle pas le ocaml couramment)
Sinon très bonne dépêche !
[^] # Re: Coquille ?
Posté par octachron . Évalué à 1.
Bien vu, ce
name
a effectivement échappé au renommage enname_opt
.[^] # Re: Coquille ?
Posté par claudex . Évalué à 3.
Corrigé, merci.
« Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche
# Coquilles
Posté par Snark . Évalué à 2.
J'ouvre la traditionnelle enfilade des coquilles signalées:
"n'ont pas encore débouché" sans 's'
[^] # Re: Coquilles
Posté par Snark . Évalué à 1.
"la plupart des utilisateurs final" ? Est-ce que le "final" non accordé sert à quelque chose?
[^] # Re: Coquilles
Posté par claudex . Évalué à 3.
Corrigé, merci.
« Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche
[^] # Re: Coquilles
Posté par claudex . Évalué à 3.
Corrigé, merci.
« Rappelez-vous toujours que si la Gestapo avait les moyens de vous faire parler, les politiciens ont, eux, les moyens de vous faire taire. » Coluche
[^] # Re: Coquilles
Posté par Snark . Évalué à 1.
"comme le montre les exemples" -> "comme le montrent les exemples"
[^] # Re: Coquilles
Posté par Benoît Sibaud (site web personnel) . Évalué à 3.
Corrigé, merci.
[^] # Re: Coquilles
Posté par Storm . Évalué à 1.
utiliser un algorithme générique -> utiliser un algorithme génétique (vérifié sur la première ligne de la page de afl)
# Chaînes de caractères immutables
Posté par GNU_Eths . Évalué à 1.
Les chaînes de caractères immutables ont été introduit avec OCaml 4.02 et pas OCaml 4.03.
[^] # Re: Chaînes de caractères immutables
Posté par Benoît Sibaud (site web personnel) . Évalué à 3.
Corrigé, merci. D'ailleurs c'était précisé dans la dépêche sur OCaml 4.02.
# Expressivité du langage
Posté par chimrod (site web personnel) . Évalué à 10.
En voyant les projets graviter autour du langage, ce qui m'interpelle le plus avec ce langage, c'est son expressivité. Quand je vois les exemples sur la page du projet je me rend compte que la force du langage tient dans sa capacité à typer les données (pour ensuite les exprimer dans un autre langage par exemple).
Naïvement, on pourrait dire qu'il est toujours possible d'exprimer un langage fortement typé dans un langage moins fortement typé, et qu'OCaml impose des contraintes lors de l'écriture du code pour indiquer au compilateur le maximum d'informations sur les variables, sauf que je ne ressent jamais cette contrainte en écrivant en OCaml. Au contraire, lorsque je passe du code OCaml à du code Java (par exemple) j'ai l'impression de bégayer tellement j'écris du code inutile (oui mon tableau de string est bien un tableau de string, je viens de l'écrire !).
La plus grande force du langage selon moi vient de là : avoir pu conserver une telle expressivité, avec un minimum d'indications lors de l'étape d'écriture du code.
# Coquille : un gestionnaire qui ne gère qu'un élément
Posté par RyDroid . Évalué à 1.
[^] # Re: Coquille : un gestionnaire qui ne gère qu'un élément
Posté par Benoît Sibaud (site web personnel) . Évalué à 3.
Corrigé, merci.
# Reason
Posté par Eiffel . Évalué à 4.
Même si ça dénature un peu le langage (pour moi la syntaxe d'un langage est une grosse part de son identité) je trouve ce projet intéressant et je me demande même s'il ne serait pas possible de l'étendre à d'autres langages.
On pourrait aller plus loin en imaginant pouvoir écrire des front-ends analyseurs syntaxiques pour n'importe quel compilateur qui permettrait de profiter des spécificités d'un langage (optimisation, interprétation, etc.) sans avoir à en connaître la syntaxe.
[^] # Re: Reason
Posté par Ontologia (site web personnel) . Évalué à 4. Dernière modification le 17 juillet 2017 à 14:58.
Tu risquerais de tomber dans des subtilités sémantiques des langage qui existent dessous : la sémantique objet est totalement différente entre Java et OCaml par exemple, car en OCaml, une classe héritant d'un autre n'est pas forcément son sous type.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Reason
Posté par Eiffel . Évalué à 1.
J'ai pensé après coup qu'il y aurait sûrement des difficultés, par exemple en utilisant la syntaxe d'un langage non objet pour "écrire" un langage objet.
Après mon poste était vraiment un poste d'idéaliste rêveur :)
[^] # Re: Reason
Posté par kantien . Évalué à 7.
Ce qui est conforme à la nature des choses : l'héritage est une notion syntaxique et le sous-typage une notion sémantique.
Par exemple, lorsque l'on écrit le syllogisme suivant:
le concept « homme » est un sous-type du concept « animal » (ce qu'exprime la mineure). Malheureusement, les adeptes de la POO présentent souvent les concept de classes et d'héritage ainsi, ce qui est une erreur.
Oleg Kyseliov a illustré, sur sa page Subtyping, Subclassing, and Trouble with OOP, le genre de bugs difficiles à détecter que cette confusion peut engendrer. Son exemple est en C++ (mais ça marche aussi en Java, Python…) et traite des ensembles (Set) comme sous-classe des multi-ensembles (Bag).
Il faut prendre soin, dans la relation de sous-typage, des problématiques de covariance et de contravariance. Les règles de la relation de sous-typage sont exposées dans ce chapitre de Software Foundations de Benjamin C. Pierce. La première règle, par exemple, dite règle de subsomption :
est celle que l'on utilise dans le syllogisme :
homme <: mortel
)Socrate : homme
)Socrate : mortel
).La règle suivante, la règle structurelle, est celle qui est utilisée dans mon premier syllogisme avec les types animal, mortel et homme.
Les problèmes de covariance et de contravariance arrivent lorsqu'il faut sous-typer des fonctions (méthodes dans les objets), dont la règle est :
autrement dit la flèche inverse la relation de sous-typage sur ses domaines (
T1 <: S1
), elle y est contravariante; tandis qu'elle la conserve sur ses codomaines (S2 <: T2
), elle y est covariante.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 1. Dernière modification le 18 juillet 2017 à 01:56.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à -1. Dernière modification le 18 juillet 2017 à 07:57.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Reason
Posté par Def . Évalué à 7.
Je vais essayer d'expliquer rapidement, mais il y a des ouvrages entiers sur la question. Si l'on souhaite vraiment comprendre il faut aller plus loin.
Héritage
Donc "l'héritage", c'est récupérer du code écrit ailleurs. C'est pas bien différent d'un simple "#include" (après l'implémentation peut-être plus complexe qu'une simple substitution de texte, mais c'est un détail).
Sous-typage
Le sous-typage, c'est déterminer quand tu as le droit d'utiliser un objet à la place d'un autre (le contexte attend un X mais toi tu peux fournir un Y : est-ce correct ou pas ?).
Un petit exemple en supposant que B est un sous-type de A (peu importe comment la relation "être sous-type de" est définie dans le langage).
Tu implémentes une méthode qui renvoie un A (parce que tu hérites d'une classe qui a défini cette méthode comme renvoyant A). Tu as le droit de renvoyer éventuellement un peu plus (un type plus précis), un B est acceptable :
- pour les utilisateurs de la classe héritée, ils auront accès au type le plus précis, ils pourront profiter des fonctionnalités de B ;
- pour les utilisateurs qui accède à la méthode par la classe parente, ils attendent un A, mais il est correct de considérer cette valeur de type B que tu as renvoyé au type A, ils sont contents.
A contrario, si cette méthode reçoit un argument de type B mais dont tu n'utilises que les méthodes définies dans A, tu peux oublier que c'est un B et être plus général en ne demandant qu'un A. Le raisonnement ci-dessus s'applique dans l'autres sens (les utilisateurs de la classe parente devront toujours fournir un B, c'est pas grave, les utilisateurs de la classe fille auront la privilège de n'avoir qu'un A à fournir).
Donc dans certains contextes pour être un sous-type, il faut qu'un certain type soit plus précis, dans d'autre il faut qu'il soit plus général.
Les contextes il faut être plus précis sont dits covariants, car le contexte varie dans le même sens que le type (je suis plus préçis si mon type de retour est plus préçis).
Les contextes il faut être plus général sont dits contravariants, car le contexte varie dans le sens opposé à ce type (je suis plus préçis si mon argument l'est moins).
Plus généralement, pour être plus "fort", il faut consommer moins d'informations et en renvoyer d'avantage.
Sous-typage nominal
Jusque là c'est de la logique, un dialogue entre appelants et appelés dans les langages de programmations.
La logique permet de distinguer ce qui a du sens ou pas. On pourrait se dire qu'un langage de programmation peut n'en faire qu'à sa tête et suivre d'autres règles, mais on ne peut vraiment y échapper, ça conduirait à des "Runtime Type Error" : pour être correct il faut au moins faire ça.
Si l'on considère que l'héritage définit le sous-typage (on dit sous-typage nominal parce que pour savoir si une classe est sous-type d'une autre, on prend les noms des deux classes et on regarde où ils se trouvent dans le diagramme d'héritage), on va se retrouver dans une situation pas très confortable:
1) Pour commencer, la relation de sous-typage est très grossière, ce sont juste des noms. On voudrait peut-être quelque chose de plus fin, ben on peut pas. Enfin des fois c'est mieux de ne pas donner trop d'outils au développeur.
2) Comme héritage et sous-typage coïncide, on ne peut pas réutiliser de code sans récupérer toutes les contraintes énoncées au dessus.
3) Ou alors on décide d'ignorer les contraintes. Les systèmes de types des langages objets ne sont en général pas très fins pour commencer, donc c'est pas très grave on peut s'en sortir un certain temps sans être amené à des incohérences (au pire on "cast").
Notez que ce n'est pas vraiment une solution recevable : comme on a sous-spécifié le problème, il y a plus de solutions. L'aboutissement est un langage "typé dynamiquement": avec un seul type, on ne risque pas de créer d'incohérences.
Cela conduit évidemment a des désastres, on encourage donc quand même informellement les règles logiques ci-dessus avec le principe de substitution de Liskov.
Sous-typage structurel
En OCaml il n'y a pas de cast, donc on ne peut pas contourner les contraintes logiques. Par contre son système de type (le langage utilisé pour la spécification logique) est suffisamment expressif pour être utilisable sans ces casts: on se retrouve parfois à devoir spécifier précisément, ou bien face à ses propres incohérences et cela aide beaucoup à concevoir une hiérarchie d'objets pas bancale (quitte à la traduire dans un autre langage a posteriori).
Enfin plutôt que de se restreindre à des noms, OCaml utilise le sous-typage structurel: le sous-typage ne va considérer que les parties d'un objet (représentées par une liste de méthodes) utilisé par un code pour déterminer les contraintes qui s'appliquent. Cette pratique est informellement appelée "duck-typing".
Le principe de substitution sera respecté par construction, à la granularité de spécification que permet le langage de type d'OCaml.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à -4. Dernière modification le 18 juillet 2017 à 19:32.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Reason
Posté par BAud (site web personnel) . Évalué à 3.
justement, non. Relis à tête reposée :-) Ne pas confondre l'hypothèse de départ pour la remettre en conclusion. Faux + Faux n'implique pas vrai ('fin si, mais bon c'est l'absurdité de la logique…).
[^] # Re: Reason
Posté par kantien . Évalué à 8.
Effectivement, je me rends compte que ce que j'ai écrit doit paraître abscons pour qui n'est pas habitué à ce genre de questions. Je veux bien essayer de clarifier la chose en étant plus didactique, et compléter ainsi la réponse de Def.
On va partir de la logique et de sa notion de concept, la POO cherchant à procéder à une classification des concepts en genres et espèces comme les biologistes le font pour le règne animal.
On peut voir les types comme signifiant des concepts et les termes d'un langage comme des choses rentrant sous un concept. Par exemple, avec le concept de « verre » on peut dire, en en montrant un, « ceci est un verre ». Dans une telle situation, les logiciens disent que l'on subsume la perception que l'on a (l'intuition) sous le concept de « verrre ». Il en est de même lorsque l'on dit que Socrate est un homme. En théorie des types, un tel jugement est appelé un jugement de typage et on l'écrirait
Socrate : homme
. Comme dans l'exemple suivant :Je définit une variable
i
, et la boucle REPL OCaml me répond : la valeuri
est unint
.Jusque là, c'est ce que tu avais bien compris de la notation
t : T
. Ensuite dans le pensée, nous hiérarchisons nos concepts en genre et espèce : les hommes sont des mammifères, les mammifères sont des animaux, les animaux sont des êtres vivants…Ainsi, par exemple, un triangle est une espèce de polygone et le concept de polygone constitue le genre dans le rapport de subordination logique entres les deux concepts.
Je pense (du moins je l'espère) que ce que je viens d'exposer doit être facilement compréhensible. Les langages orientés objets prétendent, via leur système de classe et d'héritage, réaliser une telle hiérarchie des concepts en genre et espèce. Sauf que, dans les faits, c'est logiquement faux dans la plupart des langages donc faux.
Ce rapport respectif entre concepts, le rapport entre genre et espèce, est justement ce que l'on appelle la relation de sous-typage que l'on note
S <: T
pour dire queS
est un sous-type deT
. En revanche, une sous-classe (si l'on entend par là une classe qui hérite d'une autre) n'est pas nécessairement un sous-type. Comme l'a dit Def dans sa réponse, l'héritage c'est proche d'un simple#include
, ça évite le copier-coller : c'est pour cela que je parlais de notion syntaxique.Venons-en maintenant aux règles qui déterminent la relation de sous-typage. Les deux premières que j'ai données sont issues de la syllogistique aristotélicienne : la première figure. Leur notation est empruntée à la formulation par Gentzen du calcul des séquents. On y sépare verticalement les prémisses et la conclusion de la règle de déduction. Ainsi la règle :
se lit : sous les prémisses que
S
est un sous-type deU
et queU
est un sous-type deT
, on conclue queS
est un sous-type deT
. C'est la figure Barbara des syllogismes aristotéliciens.Pour la première règle, dans la prémisse
Gamma |- t : S
, le signe|-
(qui est unT
couché) se lit « thèse de ». Il signifie que, dans le contexte des hypothèses que constitue Gamma, on peut prouver la thèset : S
(que le termet
est de typeS
). D'un point de vue programmation, on peut voir Gamma comme un contexte, une portée lexicale (scope). Ainsi dans l'exemple suivant :Dans le contexte global, la REPL infère que
i : int
. En revanche, dans le contexte de définition dej
, elle inférera quei : float
. Ainsi la règle :peut se lire : dans un contexte où on peut prouver que le terme
t
est de typeS
et queS
est un sous-type deT
, on peut alors prouver, dans le même contexte, quet
est de typeT
.Voyons un peu maintenant ce qui se passe avec des objets (au sens du paradigme orienté objet), l'héritage et la relation de sous-typage. Les objets peuvent être vus comme des enregistrement extensibles (extension obtenue via l'héritage).
Prenons par exemple ces deux types OCaml :
Bien que le type des
pt3d
contiennent les champsx
ety
, on ne peut pas, en OCaml, utiliserp'
là où le système attend un objet de typept2d
.Les enregistrements OCaml ne possèdent pas cette relation de sous-typage
<:
. Pour cela, il faut passer par les enregistrements extensibles que sont les objets.On peut noter au passage que la coercition entre types doit être explicite (il n'y a pas de cast implicite en OCaml) et qu'elle est notée comme la « symétrique » de la relation de sous-typage :
:>
.Les règles qui dictent la relation de sous-typages entre enregistrements sont données dans la section records du chapitre de l'ouvrage de Benjamin C. Pierce. En gros, pour être un sous-type, il faut avoir au moins les mêmes champs (ici
x
ety
) et que les types de ces champs soient des sous-types des champs correspondant (ici ce sont les même, à savoirfloat
).C'est ici qu'il peut y avoir des soucis entre héritage et sous-typage. Pour l'instant nos méthodes n'étaient pas des fonctions. Lorsque l'on a une classe qui possèdent des fonctions comme méthodes, au moment de l'héritage il faut contrôler le sous-typage entre ces fonctions. D'où la règle de sous-typage entre fonctions et les problématiques de contravariance et de convariance.
Commençons avec deux classes simples à la mode fonctionnel : des points à une ou deux dimensions avec des méthodes pour les déplacer.
Ici les méthodes
move_x
(oumove_y
) font référence au types de l'objet ('a
) : elle retourne un objet de même type que l'objet sur lesquelles on les utilise. Comme ce type apparaît en position covariante (sortie), l'héritage est aussi un sous-typage.Maintenant, au lieu de considérer des points, considérons des vecteurs à une ou deux dimensions disposant d'une méthode pour les ajouter entre eux (opérateur binaire).
Ici la méthode
add
n'ont seulement renvoie un objet du type de la classe (position covariante) mais en prend également un en entrée (position contravariante). Ici l'héritage ne sera pas identique au sous-typage.Pour que le type
vect2d
soit un sous-type du typevect1d
, il faudrait que sa méthodeadd : vect2d -> vect2d
soit un sous-type de la méthodeadd : vect1d -> vect1d
du typevect1d
. Ce qui, d'après la règle de sous-typage des fonctions, nécessiterait quevect2d
soit à la fois un sous-type et un sur-type devetc1d
, ce qui est impossible.Pour rappel, la règle en question était :
autrement dit, avec les prémisses que
T1
est un sous-type deS1
et queS2
est un sous-type deT2
, on en conclue que le type des fonctions deS1
versS2
(notéS1 -> S2
) est un sous-type de celui des fonctions deT1
versT2
. La règle se comprend intuitivement ainsi : si j'ai une fonction qui prend unS1
, je peux bien lui donner également unT1
étant donné queT1 <: S1
(si j'ai besoin d'un animal, prendre un homme convient aussi); et si je renvoie unS2
alors a fortiori je renvoie aussi unT2
(si je renvoie un chat, je renvoie aussi un félin).Dans le cas de la méthode
add
de la classevect2d
, on voit bien le problème : pour fonctionner elle a besoin d'un attributy
sur son entrée, ce que ne peut lui fournir un objet de la classevect1d
.J'espère avoir été plus clair sur la distinction entre héritage et sous-typage. Si ce n'est pas le cas, et que tu as encore des questions, n'hésite pas. Pour plus d'information, voir aussi la page du manuel OCaml sur les objets.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Reason
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
Et par rapport à la logique, si j'ai bien compris l'origine du lambda calcul, c'est les incohérences de la théorie des ensembles qui ont donné la théorie des catégories (?) puis le lambda calcul, mais quel rapport ici, entre le typage est la logique. Le typage définit un ensemble de "vérité", et le compilateur vérifie la cohérence de l'ensemble ? Pourquoi les littéraux sont définit de manière spéciale par rapport au typage, c'est une question de facilité, ou est-ce qu'il y a une vrai différence de nature ?
"La première sécurité est la liberté"
[^] # Re: Reason
Posté par kantien . Évalué à 4.
J'ai hésité avant de te répondre pour plusieurs raisons. Tout d'abord il y a des questions d'ordre historique sur lesquelles je ne sais pas tout, ensuite je craignais de faire encore une réponse à rallonge assez rebutante, et enfin je n'ai pas compris ta dernière question sur les littéraux. Je vais essayer de répondre comme je le peux, sans faire trop long.
Sur le plan historique, les paradoxes de Burali-Forti et Russell dans la théorie des ensembles de Cantor-Frege ont donné naissance à l'axiomatique de Zermelo-Fraenkel. C'est plutôt dans ce cadre axiomatique (avec quelques variantes) que l'on pratique de nos jours la théorie des ensembles.
De leur côté, Russel et Withehead écrivirent les Principia Mathematica pour tenter de fonder l'édifice mathématique sur la seule logique. C'est leur notation utilisée pour les fonctions propositionnelles qui inspira Church pour son lambda-calcul. Ils notaient la proposition
f
appliquée à un objet singuliera
:fa
, et la fonction qui à un objeta
indéterminé faisait correspondre la valeur de véritéfa
ainsi :fâ
. Ils avaient aussi une notation du type :âfa
. Comme l'éditeur de Church ne pouvait pas mettre d'accents circonflexes sur toutes les lettres, ils ont remplacer l'accent circonflexe par un lambda majuscule qui est ensuite devenu un lambda minuscule. Et l'on note depuis la fonctionx -> f x
ainsi : .La théorie des catégories fut introduite originellement dans le cadre de la topologie algébrique. Elle avait pour but d'étudier les relations entres structures mathématiques qui préservent certaines propriétés des dites structures : les morphismes. Ce n'est qu'ensuite qu'un lien a été fait avec la logique et la sémantique des langages de programmation.
En ce qui concerne le lien entre typage et logique, cela concerne la théorie de la démonstration. Il y a un bon ouvrage de vulgarisation sur la logique : La logique ou l'art de raisonner qui expose simplement les différents point de vue sur la logique. Le plan de l'ouvrage est en quatre parties :
La notion de vérité relève de la seconde partie, celle sur l'interprétation, et fait intervenir la notion de modèles dont s'occupe la théorie des modèles. Pour prendre un exemple simple. Si on prend un langage qui dispose d'une fonction binaire (disons
+
) et de deux constantesI
etII
. Alors si on interprète l'énoncéII + II = I
dans l'ensembleN
des entiers naturels, munis de son addition et en associant1
àI
etII
à2
, alors cet énoncé sera faux. En revanche si on fait de même dans le groupeZ/3Z
alors il sera vrai. Dans cette branche de la logique, on développe la notion de modèle d'une théorie et celle de conséquence sémantique : si un énoncé est vrai dans tout modèle d'une théorie alors on dit qu'il est une conséquence sémantique de la théorie. Dans l'ouvrage sus-cité, ils écrivent une des choses les plus importante à comprendre : « […] quand il existe une structure naturelle pour interpréter les énoncés (par exempleN
dans le cas des énoncés arithmétiques), il est nécessaire d'envisager toutes les autres, même celles qui semblent n'avoir aucun rapport intuitif avec les énoncés. C'est en faisant varier les interprétations possibles, et en constatant que certaines notions ne sont pas sensibles à ces variations, que l'on touche à l'essence de la logique ». (Tu pourras penser, par exemple, à mon journal sur l'interprétation avec la méthode tagless final où je faisais plusieurs interprétations pour un même terme syntaxique).De son côté la théorie de la démonstration avec ses formalismes comme la déduction naturelle ou le calcul des séquents de Gentzen, ou les systèmes à la Hilbert, ne s'occupe pas du rapport que les énoncés entretiennent avec des objets (modèles) mais seulement du rapport que les jugements (ou énoncés) entretiennent entre eux. Son cheval de bataille, c'est l'inférence : à quelles conditions peut-on inférer une conclusion donnée de prémisses données ? On obtient alors la notion de conséquence déductive : un énoncé est une conséquence déductive d'une théorie si on peut l'établir comme conclusion d'une preuve dont les prémisses sont toutes des axiomes de la théorie. Les deux questions qui se posent alors sont :
La première a trait à la cohérence du système (on ne peut pas trouver tout et n'importe quoi avec) et la seconde a trait à sa complétude (il peut prouver tout ce qui est prouvable) qui renvoie à un théorème fameux de Gödel (moins connus que son théorème d'incomplétude, mais tout aussi important).
C'est cette deuxième branche de la logique qui est en lien avec le typage des langages de programmations, elle donne lieu à la correspondance de Curry-Howard ou correspondance preuve-programme : le type d'un programme est une énoncé dont le programme est une preuve. Ce qui apporte de la sécurité dans l'écriture de code, comme le montre le chapitre sur les systèmes de type du livre de Benjamin C. Pierce : well typed programm never gets stuck, autrement dit un programme bien typé ne se retrouvera jamais dans un état indéfini où aucune transition n'est possible. Puis, selon la richesse d'expressivité du système de type, il permet d'exprimer au mieux la sémantique du code : il limite les interprétations possibles, via la complétude.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Reason
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
Réponse bien complète :)
Concernant les littéraux, je ne comprends pas pourquoi il sont considéré différemment du type.
En gros si tu as
i : int
i + 1
i + 1 est ok, uniquement car on détermine que 1 est d'un type entier.
Or a part dans fonctionnalité de généricité, le type n'est jamais une variable. C'est chiant dans ingénierie des modèles, tu ne peux pas prévoir un modèle de plus haut niveau, qui sera utilisé pour en faire un de plus petit niveau en définissant le type de certain donné par exemple. Ce genre de problème se contourne en réinventant une sorte de typage depuis le modèle de haut niveau, mais c'est moche et lourd. De plus, la vérification des types doit être réécrites.
Cela se retrouve dans tout ce qui ressemble à des déclarations des schémas (xml ou autre) : il est compliqué d'avoir un schéma dans le même "monde" (au sens d'une library ou d'une autre donné) qu'une instance d'un objet. c'est ainsi que l'on se retrouve avec des "metamodèles" (en UML) qui devienne super chiant quand il s'agit de rapprocher des modèles utilisant des metamodèles différents, ce qui ne poserait aucun problème si on utilisait une library à la place.
"La première sécurité est la liberté"
[^] # Re: Reason
Posté par kantien . Évalué à 2. Dernière modification le 18 août 2017 à 11:35.
Je ne vois toujours pas où tu veux en venir, et ce que tu veux dire par « les littéraux sont considérés différemment du type ». Le langage possède des types primitifs comme
int
,float
,char
oustring
et l'on utilise des littéraux pour construire des valeurs de ces types.Pour ton exemple, le type checker arrive bien à la conclusion :
qu'est-ce qui te chagrine là-dedans ? Que le compilateur considère que
1 : int
? Mais c'est là le principe des types primitifs et des littéraux.Ta question se situe peut-être ici. Un type est bien une variable dans le cas de la généricité : les types paramétriques sont des fonctions des types vers les types, c'est le principe des constructeurs des variants :
ici on a une fonction récursive, définie par cas, à un paramètre des types dans les types qui définie le type des listes chaînées.
Ce qui te pose problème, c'est quoi ? Que l'on n'ait pas de fonction des termes dans les types ? Là où il y a des fonctions des termes (ou valeurs) dans les termes et des fonctions des types dans les types ? Mais ça c'est le typage dépendant, et il faut passer à Coq. Ou alors je n'ai vraiment pas compris ta question.
Pour le reste, ne connaissant pas les domaines de l'ingénierie des modèles, des schéma XML ou UML, je ne peux rien en dire. Il faudrait que tu présentes un cas simple et concret, et non des généralités, pour que je comprennes où tu veux en venir.
Pour un kantien, la complétude est une quête sans relâche. Dans sa dépếche sur Coq 8.5, Perthmâd signalait que, en vertu de la correspondance preuve-programme, le théorème de complétude de Gödel (que j'ai mentionnait précédemment) correspondait à un décompilateur (ou désassembleur). Kant1, de son côté, ce n'est pas du code mais la structure formelle de l'esprit humain qu'il a désassemblé, selon un procédé analogue à celui qui se trouve à la base du lambda-calcul typé. :-)
je signale, au passage, que ce n'est pas moi mais Dinosaure qui a mis l'image sur la Critique de la Raison Pure dans le corps de la dépêche. ↩
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Reason
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
Tu m'as un peu largué dans les types paramétriques.
Le problème dont je parle relève bien de ingénieries des modèles, j'avais l'impression que du point de vue du code, ce n'est qu'une structure de donné (à la con).
Imagines que tu dois documenter des messages qui circulent sur un bus de communication. Tu as une lib de base "définition des champs d'octet d'un message de communication". Elle contient, des informations comme : nom, offset et taille de champ, type du champs. Ensuite, tu veux faire le boulot pour une techno de bus particulière A429, tu va réutilisé cette lib pour dire que les 3 premiers bits ont tel nom, et ont une valeur fixe, et champ de donné de type int (genre un champ d'adresse sur 8 bits, et un champs de donné sur 18 bits).
Pour une instance particulière de ce bus A429, tu va réutiliser la lib de description A429, définir des types de messages, avec des champs fixes (littéraux) et d'autres dépendantes du message (genre le message de vitesse est à l'adresse 121 fixe, mais le contenu est un entier 16 bits en km/h, en virgule fixe avec 6 bits après la virgule).
Chaque lib peut être vue comme le type de la lib qui l'utilise, ce n'est pas une transformation de type vers un autre. C'est ce mélange entre type de base et littéraux qui est impossible et très chiant en pratique.
Tu me dis pourquoi se faire chier avec un système aussi compliqué ? Le coté formel permet plein de choses. C'est pratique pour vérifier que parmi les 1000 messages échangés sur un bus, l'émetteur et le receveur reçoivent la vitesse dans la bonne unité et dans le bon encodage. Voir que dans le cas contraire, de générer un convertisseur à la volé. Cela permet de générer de la documentation propre non ambigüe. Cela permet aussi de générer du code de génération de trame (ton "float64 speed" dans un code C, a mettre au bon endroit dans le message).
J'avais déjà essayé d'en parler sur linuxfr. J'ai tenté de faire un langage de description qui permet de faire. L'idée de base est simplement d'ajouter un opérateur "est compatible avec le type de", je le notait '~' ou même '=' dans les définitions.
Ainsi, tu écris 'int ~ 1 ~ Name "a"', pour définir un truc du nom de "a" qui est de type int et vaux 1. Cela permet de le composer en plusieurs fois.
Genre 'Ref "a" ~ 2', la référence à "a" dont on ajoute 2, ce qui est faux.
Ainsi je peux définir Name "message" ~ (Name "adresse" ~ int & Name "data") dans une lib de base.
Puis Name "messageVitesse" ~ Ref "message" ~ (Ref "message/adresse" ~ 121 & Ref "message/Data" ~ (Name "Value" ~ int && Name "unit" ~ ("km/h" || "m/s") )) dans une lib plus précise. Puis Name "MessageBusTartenpion" ~ (Ref "messageVitesse" ~ (Ref "message/data/unit" ~ "km/h") || Ref "messageDistance" ) etc…
Tu peux aussi gérer plusieurs noms ou des alias 'Name "Vitesse" ~ Ref "messageVitesse"'.
La où cela devient marrant, c'est si on introduit la négation. Genre int ~ (! 0), pour faire un entier qui n'est pas nulle.
J'avais tenter de faire un type checker de façon simple en Ocaml, c'est un boulot énorme. Je voulais le refaire en tagless qui me parait super puissant, mais je n'ai pas eu le temps. Ce langage que j'appelais "Grape" (ou Cherry mais je n'assume plus :) permet de remplacer le xml, la description d'un schéma et rajoute la notion de nommage pour faire des graphs orienté et pas seulement des arbres de données. Cela permet de faire la même chose que l'UML ou SysML mais en beaucoup plus simple et de façon formelle.
Depuis, j'ai aussi un peu changer d'avis : il n'est pas possible de "mélanger" les modèles. Si on peut jouer avec des types un "peu" différent, avec un typage "weak", il reste le problème de compositions structurelles que l'on ne peut pas mixer (par exemple, un modèle de donné l'UML et sa représentation graphique en widget ). En fait, il faut faire de la transformation de modèle vers un autre (description des messages vers sa représentation html avec une lib html comme base). On peut aussi avoir la même chose décrite avec 2 normes différentes (beaucoup de standard arrivent avec leur metamodèle UML). Mixer les 2 normes est complexe et si une troisième arrive… C'est plus simple de prévoir des transformations. Cela implique des aller-retour, et de la gestion de différence. Mais je n'ai pas encore de solutions, surtout si on part du principe que le modèle est gigantesque :)
"La première sécurité est la liberté"
[^] # Re: Reason
Posté par kantien . Évalué à 3. Dernière modification le 21 août 2017 à 11:14.
Je dois avouer que je suis moi même perdu en essayant de comprendre ce que tu écris et ce que tu veux faire. Au départ, j'essayais de comprendre ce que tu voulais dire par : « les littéraux sont considérés différemment du type ». Veux-tu dire par là que les valeurs, comme
1
, et les types, commeint
, vivent dans des mondes différents ? Mais une telle situation est présente dans la quasi totalité des langages, à l'exception des langages avec types dépendants (comme Coq).Ensuite tu as écrit : « Or a part dans fonctionnalité de généricité, le type n'est jamais une variable », et c'est là que j'ai explicité, à ma façon, ce que je comprenais d'une telle phrase; d'où mon texte sur les types paramétriques.
En OCaml, on peut définir une valeur comme un couple d'entier ainsi :
On peut également définir un alias du types des couples sous la forme d'un type paramétré ainsi :
Ce type paramétré peut être vu comme une fonction des types dans les types à deux paramètres. La syntaxe Reason modifie la manière d'écrire de tels types en utilisant une syntaxe similaire à celle des fonctions :
Vois-tu l'analogie qu'il y a entre des fonctions entres valeurs et les types paramétriques (fonctions entre types) ?
Ensuite viens la chose qui semble te déranger et que tu exprimes ainsi dans ton dernier message :
Que veux tu faire ? Veux-tu que ton opérateur
~
ait comme premier paramètre un type (int
dans ton exemple) et comme second paramètre une valeur de ce type (1
dans ton exemple) ? Ce qui fait de ton exemple, une autre manière d'écrire :Mais si c'est bien ce que tu cherches à faire (avoir des fonctions qui prennent en paramètre aussi bien des types que des valeurs) alors tu cherches à avoir un système de types dépendants. Voici comment sont définies les listes polymorphes homogènes en Coq :
Sur cette structure de donnée, on peut définir la fonction
repeat
ainsi :Ici le premier paramètre de la fonction
repeat
est un typeX
, le second un termex
de typeX
et le troisième un termecount
de typenat
. On peut ainsi écrire :Autrement dit on peut mélanger types et littéraux sans problèmes. Est-ce cela que tu veux ?
Je n'ai jamais dit « pourquoi se faire chier avec un système aussi compliqué ». Déjà, je ne considère pas Coq comme étant aussi compliqué qu'on veut bien le faire croire. C'est certes plus compliqué, mais aussi bien plus puissant, que OCaml mais sans être pour autant aussi complexe que sa réputation le laisse entendre. Enfin, au sujet des possibilités des approches formelles : tu prêches un convaincu ! La formalisation de la pensée, c'est synonyme de rigueur intellectuelle pour moi; et si c'est bien fait, alors effectivement cela ouvre de grandes possibilités.
Pour reprendre un de tes exemples
le type des entiers non nuls se définie ainsi en Coq :
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Reason
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
Oui, c'est exactement ça. Et c'est chiant.
Oui (je ne connais pas coq), mais cela n’empêche pas d'être très gênant.
C'est une figure de style, désolé.
C'est ce que je connaissais des types paramétriques. Le problème est que d’accepter n'importe quoi comme équation booléenne rend la vérification très compliquée. L’intérêt de rester dans des types plus classiques est de simplifier. J'avais lu que la vérification formelle ne marche plus dés qu'il y a des multiplications dans une équation car le nombre des possibles explosent.
Si cela se trouve mon "langage" peut se traduire directement en coq.
Oui, même si je voulais juste avoir un langage de description qui m'a l'air bien plus simple que du coq, mais je me trompe peut-être. coq me semble trop complexe pour être utilisé par n'importe qui.
"La première sécurité est la liberté"
[^] # Re: Reason
Posté par kantien . Évalué à 2.
En dehors du fait de recourir à un système de types dépendants, je ne vois pas comment on peut mélanger types et valeurs ensembles. On peut mélanger des types avec des types en C++ avec les templates, en Java avec les generics, en Haskell ou OCaml avec les types paramétrés. Mais mélanger des types et des valeurs comme paramètres de fonctions, c'est ce que font seuls les types dépendants. Je ne sais si c'est très gênant, mais cela ne permet effectivement pas d'exprimer certaines contraintes logiques dans le système.
Ce n'est pas une équation booléenne. Le terme
n <> 0
(ounot (n = 0)
) n'est pas un booléen mais une proposition.Les propositions sont susceptibles d'être prouvées (ou non), mais ce ne sont pas des booléens qui valent
true
oufalse
.Ainsi un habitant du type
non_nul
est la donné d'une valeurn
de typenat
ainsi que d'une preuve qu'elle est non nulle. Voir le paragraphe Propositions and booleans de Software Foundations. Se représenter la logique comme un calcul sur les booléens est une vision réductrice de cette science.Lors de la traduction de Coq en OCaml, tout les habitants du type
Prop
sont effacés : ils servent à exprimer la spécification du code mais disparaissent à la compilation, de la même façon que les informations de typage disparaissent à la compilation en OCaml.Si on ne veut pas aller jusqu'à utiliser Coq pour réaliser ce genre de chose, il est toujours possible de faire quelque chose d'approchant en OCaml avec les GADT. Mais cela relève déjà d'un usage avancé du système de types. Voir le chapitre 8.1.2 Depth indexing imperfect trees p.13. Les GADT servent ici à encoder des preuves qui seront construites dynamiquement (à l'exécution) et qui paramétreront le type des arbres.
Enfin tu devrais jeter un œil au système des modules et des foncteurs du langage. Lorsque tu parles d'une technologie de bus particulière A429 ainsi qu'une instance de cette technologie, cela peut peut être s'exprimer avec des signatures (définition générale de la technologie) et des modules (une implémentation particulière ce celle-ci).
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Reason
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
J'ai toujours trouvé les GADT compliqués, il faut beaucoup réfléchir pour voir comment exprimer même des trucs simples. (genre exprimer ~ en GADT, c'est pas possible, pas possible de coller des fonctions dans l'arbre en question).
Concernant le foncteur, je ne vois pas trop. Les données au final sont des arbres typés avec des liens, qui respectent les différents niveau de raffinage ou de description.Pour moi le foncteur, permet de paramétrer avec des types ou changer la définition de fonction (tagless final), même avec du tagless final, je ne vois pas trop comment tu accumules les contraintes.
"La première sécurité est la liberté"
[^] # Re: Reason
Posté par kantien . Évalué à 2.
Euh… tagless final ou GADT c'est bonnet blanc et blanc bonnet ! ;-)
Regarde bien dans mon article à la fin de la première partie. Les types des constructeurs de mon GADT sont justement ceux que je donne ensuite aux fonctions d'interprétations.
L'idée derrière la méthode tagless final est la même que celle exposée dans l'article EDSL et F-algèbres d'Aluminium95 à la différence que j'utilise des modules et non des enregistrements. Les modules sont justes des enregistrements extensibles (objets) dopés aux stéroïdes.
Après je dois avouer que je ne comprends pas trop les spécifications de ton langage, mais il faudra bien que tu écrives un type checker (qui est une interprétation comme une autre des termes du langage). De ce que je crois comprendre de ton intention, ça me fait penser aux typages des modules et foncteurs en OCaml, c'est pour cela que je les évoquaient. Mais je me trompe peut être là-dessus.
Par exemple, quand tu écris :
N'y a-t-il pas un rapport avec ce code ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Reason
Posté par Nicolas Boulay (site web personnel) . Évalué à 3.
Le plus souvent oui. Je pense juste que mon code est un poil plus léger, et rend l'indépendance plus évident.
"La première sécurité est la liberté"
[^] # Re: Reason
Posté par kantien . Évalué à 3.
Petite précision : quand j'ai dit qu'il n'est pas possible de parémétrer un type par des valeurs, ce n'est pas tout à fait vrai. C'est possible via des foncteurs, mais la garantie des invariants doit être contrôlée dynamiquement. Michaël en a donné un exemple.
On peut par exemple faire un type d'entier borné ainsi :
Ici le module
X
qui paramétrise le foncteur fournit les valeursmin
etmax
qui définisse le segment et paramétrise donc le typet
. Néanmoins il faut contrôler dynamiquement que l'on est bien dans les bornes.Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 1. Dernière modification le 20 juillet 2017 à 00:58.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Reason
Posté par BAud (site web personnel) . Évalué à 4. Dernière modification le 20 juillet 2017 à 02:12.
/hs je remarque que tu sembles dans une démarche apparemment plus raisonnée et raisonnable que « d'habitude ». J'apprécie notamment ta très bonne utilisation de Markdown pour clarifier et rendre lisible ton raisonnement. Heureux que tu perdures à revenir, cette fois-ci en donnant la grille de lecture de tes commentaires, qui — à une époque révolue j'espère — auraient pu être vus comme au mieux abscons, voire difficilement compréhensibles. J'espère que cette tendance que j'entrevois se confirmera par la suite (sans vouloir te mettre une quelconque pression).
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à -5. Dernière modification le 20 juillet 2017 à 03:12.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Reason
Posté par chimrod (site web personnel) . Évalué à 5.
Je peux me permettre d'éclaircir les deux questions que tu soulèves (et qui suscitent débat parmi les gens qui découvrent OCaml).
La notation
2.
est une version abrégée de2.0
, et permet de définir un nombre flottant.Puisqu'OCaml est un langage avec un typage très fort, ce nombre est associé avec un type :
float
. On le voit en entrant la commande dans le repl :La fonction
+
, elle de son côté, est une fonction définie ainsi (toujours obtenu à travers le repl) :C'est à dire qu'il s'agit d'une fonction, prenant un type
int
, suivi d'un deuxièmeint
, et retourne un autre typeint
(je laisse de côté la Curryfication pour l'instant), du sucre syntaxique permet d'écrire5 + 5
ou(+) 5 5
et produire le même résultat (la deuxième notation ayant l'avantage de faire correspondre l'ordre des paramètres avec le type de la fonction).Pour en revenir à notre nombre flottant, je répète que le typage est très fort, et il est inutile de chercher à donner un paramètre de type
float
à une fonction qui attend unint
. Aussi, l'addition a été définie deux fois :+
+.
(au final la même primitive C est appelée, il ne s'agit donc pas de code dupliqué).
Ça fait parti de la rigidité du langage (et peut surprendre au début), mais une fois que l'on a compris le principe, les choses sont beaucoup plus claires, ce qui est valable pour ces deux types est généralisé à tous les types que l'on peut définir dans le langage : une fonction ne peut recevoir en paramètre que les types pour lesquelles elle a été définies — il n'y a pas de conversion implicite, ni de surcharge de fonction.
[^] # Re: Reason
Posté par kantien . Évalué à 2.
Je comprends l'appréhension qu'a pu susciter ma réponse, mais dans un premier temps je n'ai pas vu comment faire plus court. Il me fallait poser les termes du problèmes (d'où l'exposition des notions de genres et d'espèces), expliquer comme lire les règles de déduction à la Gentzen et illustrer par des exemples un cas où une classe héritant d'une autre n'en était pourtant pas un sous-type.
Je vais essayer de condenser le cœur de l'argumentaire (le nervus probandi, comme on dit).
Oublions le Gamma et le code OCaml.
Laissons de côté le Gamma, qui n'est nullement essentiel pour comprendre le problème, et le code d'illustration en OCaml. L'essentiel tient déjà dans ce qui était simple à comprendre :
Ensuite on va considérer deux classes dans une syntaxe de mon invention (c'est proche de mon exemple final).
Voilà deux classes A et B, où la deuxième dérive de la première, ajoute un attribut et surcharge leur méthode commune
meth
. Pour que B soit un sous-type de A, il faudrait que les types de leurs composants communs soient des sous-types les uns des autres. Autrement dit, il faudrait queT1 <: T1
(types deattr1
) et queB -> B <: A -> A
(types demeth
).Tout type étant un sous-type de lui-même, on a bien
T1 <: T1
, mais la deuxième condition ne peut être vérifiée. En voici la raison :Or, sur le plan de la subordination des genres et des espèces, on a :
homme <: animal
etchat <: félin
. Donc en condensant les deux principes précédents et en faisant abstraction des concepts impliqués, on aboutit à la règle de déduction suivante :Ainsi pour pouvoir prouver la condition
B -> B <: A -> A
, il faudrait satisfaire les deux prémisses de la règle ci-dessus, à savoir :A <: B
etB <: A
. Ce qui reviendrait à dire que les deux classes sont identiques, ce qui n'est évidemment pas le cas.Revenons à Gamma et au code OCaml.
Ce n'est vraiment pas un point très important à comprendre, le calcul des séquents est surtout un outil qui sert aux personnes étudiant les preuves (les théoriciens de la démonstration); comme le dit la page wikipédia : « le calcul des séquents doit se penser comme un formalisme pour raisonner sur les preuves formelles plutôt que pour rédiger des preuves formelles ».
La lettre grecque dans les notations à la Gentzen sert à désigner l'ensemble des hypothèses utilisées pour prouver la thèse qui se trouve à droite du symbole . Prenons le problème de géométrie suivant :
Soit ABC un triangle isocèle en A et appelons O le milieu du segment BC. Montrer que la droite (BC) est perpendiculaire à la droite (OA).
Ici le contexte Gamma c'est l'énoncé du problème (auquel il faudra rajouter quelques axiomes de la géométrie euclidienne), et à droite du symbole de thèse on aura le résultat à prouver.
Pour tes questions sur le code OCaml, chimrod t'a en partie répondu. En ce qui concerne le syntaxe
let ... in
, c'est ainsi que l'on définit des variables locales en OCaml. Exemple dans la boucle interactive :Les variables
i
etj
n'existent qu'au sein de l'expressioni + j
, elles sont locales et n'existent plus une fois cette dernière évaluée. Cela étant la boucle me répond que la sommei + j
est de typeint
et vaut 3. Ce qui en notation de Gentzen revient à dire que le type checker a pu prouver ce séquent :Vois-tu ce qu'est le contexte Gamma dans cet exemple ?
Pour terminer ma réponse, la règle que tu cites en fin de ton message :
n'était pas celle utilisée dans mon exemple. Mon exemple avait pour but de répondre à ta question qu'est-ce que Gamma ? (à savoir un contexte, un environnement), et ensuite je réécrivais cette règle pour pouvoir la traduire en français. C'est néanmoins cette règle qui est utilisée dans un bout de code qui se situe un peu plus loin :
Dans ce contexte on sait que
op' : point2d
, de plus on a bienpoint2d <: point
, et donc le type checker peut conclure qu'on a le droit de considérerop'
comme étant de typepoint
.Reste-t-il des points obscurs dans mon exposé ?
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: Reason
Posté par djano . Évalué à 2.
Certains ont essayé avec des outils de build (polyglot maven). Je ne suis pas sûr que le succès ait été au rendez-vous.
[^] # Re: Reason
Posté par Michaël (site web personnel) . Évalué à 3.
La dépêche est excellente mais la partie sur Reason me semble passer à côté de l'essentiel. L'intérêt pour Facebook de développer Reason n'est pas de rendre la syntaxe OCaml plus ou moins facile pour le quidam moyen mais de faciliter l'apprentissage de OCaml à tous ses développeurs JavaScript: c'est une perspective bien moins large!
Je ne suis pas du tout dans le domaine de la compilation mais il me semble que ce genre de technique à toujours fait partie du domaine, avec C traduit en assembleur, C++ en C, pour citer quelques exemples relativement anciens.
# SML
Posté par robin . Évalué à 2.
Ça fait bizarre de voir ne serais-ce qu'une référence à ce langage (SML) ! Durant mon stage de fin d'étude l'an dernier, je l'ai utilisé par ce que c'était un des deux langages utilisés dans la boite ou je travaillais et de l'aveu des devs eux-même ils étaient certainement les derniers programmeurs à l'utiliser encore (conservé pour raisons historique). Bref, ça m'a fait sourire :)
bépo powered
[^] # Re: SML
Posté par gasche . Évalué à 5.
Il reste des niches où SML est assez actif, en particulier c'est le langage d'implémentation de l'assistant de preuve Isabelle qui est très bon et utilisé par une large communauté—relativement au groupe d'utilisateurs d'assistants de preuve, qui restent aujourd'hui surtout des outils académiques.
# futur
Posté par Nicolas Boulay (site web personnel) . Évalué à 9.
J'adore Ocaml, et j'aurais aimé continuer à l'utiliser grâce à son système de type, sa création/ parcours d'arbre très simple, le tagless final (présenté par kantien). C'est un outil parfait pour un "filtre unix", un programme que l'on lance une fois et donne un résultat (compilateur, transformation, documentation, calcul….).
Mais si on veut faire de la GUI, il y avait au dernière nouvelle que du gtk 2.0 de disponible qui n'utilise pas les arbres typés qui serait pourtant géniaux dans le cas d'une GUI. Bref, c'est peu conseillé.
Pour faire un serveur, il n'y a pas l'air d'avoir grand chose d'aboutis. Le projet Ocsygen avait l'air prometteur, mais si vous comprenez leur exemple, c'est que vous avais un BAC+9 en sémantique des langages ML, et ce n'est plus de l'Ocaml mais un dialecte à eux. De plus, je ne suis pas sûr que le GC se limite à des pauses courtes (<100ms) même avec 16 Go de ram, ce qui est handicapant pour un serveur. Ils ont auss un bon compilateur de Ocaml vers javascript pour l'execution du code dans le navigateur.
D'un point de vue performance, Ocaml n'utilise toujours pas le SIMD, ce qui sera possible avec l'unboxing de tableau de flottant.
Ce qui est plus problématique, surtout dans les serveurs, est le manque de gestion du parallélisme. Aujourd'hui, chaque système dispose de 4 cores minimum. "golang" peut être plus rapide que Ocaml grâce à sa bonne gestion du multi-cpu. Ocaml ne dispose toujours pas d'un bon modèle sur ce sujet (genre message passing sans copie).
Je suis passé à "Go" pour toutes ses raisons. La lib http est ultrabasique à utiliser, les performances sont bonnes et ont peu espérer faire des interfaces en HTML avec les limites que l'on connait des interfaces web. Go manque cruellement des types union, mais son typage structurel allège beaucoup le code et les dépendances.
Mozilla arrive avec Rust, qui se veut un remplaçant de C++ pour les clients lourds, avec 90% des fonctionnalités d'Ocaml et une bonne api pour la GUI.
EML (http://elm-lang.org/) est un nouveau langage ML qui se veut un moyen de forcer l'usage correct des paradigmes à la mode de javascript (react, …). Franchement, il ne lui manque que les modules pour pouvoir faire du "tagless final" pour être un sacré écosystème pour écrire des SPA (application web) (de mon point de vue).
Les développeurs d'Ocaml sont sans doute entrain de faire un choix entre combler les manques de l'écosystème ou renforcer ses points forts (on choisit souvent un outil, car c'est le meilleur dans un domaine).
"La première sécurité est la liberté"
[^] # Re: futur
Posté par Michaël (site web personnel) . Évalué à 3. Dernière modification le 21 août 2017 à 16:06.
Je fais actuellement de l'ingénierie cloud et des programmes de type sauvegarde de BDD ou migration de schéma etc., et de l'automatisation pour AWS. Et je fais tout en OCaml ;)
La situation des GUIs est assez problématique mais on peut facilement faire des interfaces simplettes avec LablTk. Il y a des gens qui utilisent Electron pour faire des programmes plus avancés mais je ne me suis jamais penché sur cette technique.
En ce qui concerne la gestion du parallélisme, il y a plusieurs cas à distinguer. Je mettrais d'un côté la parallélisme de calcul scientifique lourd par exemple utilisant 192+ cœurs ou bien des circuits programmables, dans ce cas on passe en général par des outils spécialisés qu'on contrôle avec OCaml (ou Go, ou autre), par exemple en écrivant un binding ou un programme externe. D'un autre côté il y a le parallélisme de traitement où les entrées-sorties sont le facteur limitant. Par exemple le classique server web ou bien la recherche dans une grosse base de donnés. Ici je trouve que la question du support de ce genre de parallélisme est un peu “90s” car aujourd'hui l'approche consistant à écrire des programmes à un seul fil d'exécution dont on lance de multiples copies en ajoutant un ou plusieurs processus de synchronisation (comme un répartiteur de charge ou une queue de travail) est très populaire. Les avantages de cette approche sur les fils multiples dans un même programme est que l'application est logiquement plus simple et l'augmentation de capacité se fait selon une seule variable, le nombre de processus vs. le nombre de processus * le nombre de fils. Cette technique introduit cependant des difficultés liées à la décentralisation de l'information, la mettre en œuvre peut donc mener à des problèmes difficiles de partage d'information.
Pour OCaml il existe la bibliothèque Lwt qui utilise la même approche que NodeJS où deux fils d'exécution invisibles à l'utilisateur existent, l'un s'occupe du bytecode ou de la logique du programme et l'autre s'occupe des entrées-sorties. Ainsi l'utilisateur peut penser à son application comme à un processus monofil tout en bénéficiant du parallélisme d'exécution. Combinée à des bibliothèques comme Cohttp (client et seveur HTTTP) ou webmachine, on peut facilement écrire des micro-services HTTP/JSON en OCaml.
PS.: La communauté OCaml monte en activité ces dernières années. Elle est maintenant solidement implantée dans l'industrie, ce qui présage de nombreux développements positifs pour le futur!
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.